第11章 契約による設計：信頼性の高いソフトウェアを構築する

結論

表明はクラスの意味的な性質を表す論理式であり、対応する抽象データ型の公理や事前条件を導入するために用いられる。

表明は事前条件、事後条件、クラス不変表明に利用される。この他に、表明を含む構成要素としてループ不変表明やcheck命令がある。

あるルーチンの事前条件と事後条件は、そのルーチンのクラスと顧客との間で交わされた契約と考えることができる。つまり、ルーチンコールが事前条件にしたがっている限り、契約はルーチンに対して拘束力を持ち、ルーチンは、お返しに、事後条件を保証しなければならない。

クラス不変表明は、クラスインスタンスにおける意味的な制約を表す。不変表明は、クラスのエクスポートルーチン全ての事前条件と事後条件に暗黙的に追加される。

クラスとは、抽象データ型の可能な表現を一つ記述したものである。両者の対応は、抽象化関数によって表される。これは、通常、部分関数であり逆の関係は関数でないのが一般的である。

実質不変表明は、クラス不変表明の一部であり、対応する抽象データ型に対する表現の正しさを表す。

ループは、ループ不変表明と変化表明を持つことがある。ループ不変表明は結果の性質を演繹するのに使われ、変化表明は終了を確かめるのに使われる。

クラスが表明を備えているならば、そのクラスが正しいことの意味を形式的に定義することが可能である。

表明には、以下、4つの目的がある。正しいプログラムの構築を助けること、文書化を助けること、デバッグを助けること、例外メカニズムの基になること。

ここで使った表記の表明言語は一階記述計算を含まないが、関数呼び出しを使って、たくさんの高水準な性質を表すことができる。ただし、含まれる関数は単純で、申し分ないほどに正しいものでなければならない。

不変表明と動的別名付けを組み合わせることで、間接的不変表明効果が生じる。これによって、それ自身の欠陥がなくても、オブジェクトが不変表明に違反している場合がある。